Nuprl Lemma : hd-filter
11,40
postcript
pdf
T
:Type,
P
:(
T
),
as
:(
T
List).
(
a
:
T
. ((
a
as
) & (
P
(
a
))))
((hd(filter(
a
.
P
(
a
);
as
))
T
)
c
((hd(filter(
a
.
P
(
a
);
as
))
as
) & (
P
(hd(filter(
a
.
P
(
a
);
as
))))))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
x
(
s
)
,
t
T
,
hd(
l
)
,
filter(
P
;
l
)
,
reduce(
f
;
k
;
as
)
,
if
b
then
t
else
f
fi
,
Y
,
,
tt
,
ff
,
A
c
B
,
P
Q
,
{
T
}
,
,
False
,
P
Q
,
Unit
,
P
Q
,
A
,
Lemmas
nil
member
,
l
member
wf
,
assert
wf
,
bool
wf
,
eqtt
to
assert
,
iff
transitivity
,
bnot
wf
,
not
wf
,
eqff
to
assert
,
assert
of
bnot
,
cons
member
origin